\begin{tabbing}
$\forall$$i$, $a$:Id, $T$:Type, $P$:($T$$\rightarrow$Prop).
\\[0ex]@$i$: (with ds:  action $a$:$T$ precondition $a$(v) is $\lambda$$s$,$v$. $P$($v$) s v) $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: (with ds:  action $a$:$T$ precondition $a$(v) is $\lambda$$s$,$v$. $P$($v$) s v) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ kind($e$) $=$ locl($a$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ \=(kind($e$) $=$ locl($a$) $\in$ Knd $\Rightarrow$ $P$(val($e$)))\+
\\[0ex]\& (\=$\exists$${\it e'}$:E.\+
\\[0ex]($e$ $<$loc ${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ $\in$ E \& kind(${\it e'}$) $=$ locl($a$) $\in$ Knd $\vee$ ($\forall$$v$:$T$. $\neg$$P$($v$)))))
\-\-\-\-\-
\end{tabbing}